<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01//EN" "http://www.w3.org/TR/html4/strict.dtd">
<html>
<head>
    <meta http-equiv="content-type" content="text/html; charset=UTF-8">
    <title>VOLT 2015 @ STAF</title>
    <meta name="keywords"
          content="model transformation, verification, model-driven engineering, MDE, validation, automatic test generation, UML, model-based testing, model transformation testing"/>
    <link rel="shortcut icon" href="favicon.gif" type="image/x-icon">
    <link rel="icon" href="favicon.gif" type="image/x-icon">
    <link href="data/volt.css" rel="stylesheet" media="screen">
    <script language="JavaScript">          <!--          if (parent != self)              parent.location = 'index.html';          -->      </script>
    <script type="text/javascript">            var _gaq = _gaq || [];
    _gaq.push(['_setAccount', 'UA-3117335-10']);
    _gaq.push(['_gat._anonymizeIp']);
    _gaq.push(['_trackPageview']);
    (function () {
        var ga = document.createElement('script');
        ga.type = 'text/javascript';
        ga.async = true;
        ga.src = ('https:' == document.location.protocol ? 'https://ssl' : 'http://www') + '.google-analytics.com/ga.js';
        var s = document.getElementsByTagName('script')[0];
        s.parentNode.insertBefore(ga, s);
    })();        </script>
</head>
<body>
<div align="center">
    <table class="boundary" cellpadding="0" border="0" width="750">          <!-- Banner -->
        <tbody>
        <tr>
            <td colspan="2"><img src="data/volt15banner.png" alt="VOLT 2015" width="100%"></td>
        </tr>
        <!-- Content -->
        <tr>              <!-- Menu -->
            <td class="topAligned" width="23%"><p class="sideMenu"><a class="ClassA" href="index.html">Home</a></p>

                <p class="sideMenu"><a class="ClassA" href="calls.html">Call For Papers</a></p>

                <p class="sideMenu"><a class="ClassA" href="cases.html">Cases</a></p>

                <p class="sideMenu"><a class="ClassA" href="organizers.html">Committees</a></p>

                <p class="sideMenu"><a class="ClassA" href="importantDates.html">Important Dates</a></p>

                <p class="sideMenu"><a class="ClassA" href="previousEditions.html">Previous Editions</a></p>

                <p class="sideMenu"><a class="ClassA" href="http://www.disim.univaq.it/staf2015/">STAF 2015</a></p>

                <p class="sideMenu"><a class="ClassA" href="contacts.html">Contacts</a></p>

                <p class="contents">
                <hr/>
                <h2>News</h2>
                <center> -- 20.02.2015 --<br/> VOLT 2015 website is online<br/></center>
                </p>
            <td class="contents" width="77%"><h1>Case Studies</h1>

                <p> Because verification of model transformations is a challenging topic in terms of application domains
                    and scalability, one of the primary goal of this year's VOLT edition is the quality of the
                    discussion and cross-fertilisation between different VOLT participants.
                 </p>

                <p> After three VOLT editions and a significant number of contributions in the domain of model
                    transformation verification, we see that the community has reached the maturity for comparing
                    different approaches based on common transformation verification cases. Consequently, we propose
                    specific transformation verification cases for this VOLT edition. We strongly encourage the authors
                    to apply these cases for presenting their approaches (e.g., as running examples) or for evaluating
                    their approaches (e.g., as case studies). In the vocabulary of <a
                            href="http://dx.doi.org/10.1007/s10270-014-0429-x">Lucio et al. 2014</a>, the first
                    transformation is a translation (i.e., structural bridge between DSMLs); the second is a
                    translational semantics (i.e., translation with execution delegation); and the third is a simulation
                    (i.e., operational semantics of a DSML).
                  </p>

                <p> We hope in this way to stimulate the community towards concrete, reproducible results as well as a
                    first-level comparison of tools and techniques for model transformation verification. For the
                    latter, we plan to organize a post-workshop journal article collecting the results from publications
                    of this year's VOLT edition that are taking any of the cases into consideration. </p>

                <p> We will make the following transformations together with their correctness properties available on a
                    Share repository:
                <ul>
                    <li>Translation case: UML class diagrams to RDBMS Transformation</li>
                    <li>Translational semantics case: UML Activity Diagrams to Petri nets Transformation</li>
                    <li>Simulation case: Pacman Simulation Transformation</li>
                </ul>
                </p>
                <hr>
                <h2>UML class diagrams to RDBMS Transformation Case (CD2RDBMS)</h2>

                <p><b>Transformation:</b> This case concerns the classical model transformation example dealing
                    with the generation of relational database schemas from UML class diagrams. For VOLT 2015, we will
                    consider the requirements defined by the Model Transformation in Practice Workshop 2005 (cf. <a href="http://arxiv.org/ftp/arxiv/papers/1409/1409.6611.pdf">B&eacute;zivin et al. 2014</a>) of this transformation.
                </p>

                <p><b>Metamodels:</b> UML Class Diagrams in graphical notation (CD) and Relational Schemas in graphical
                    notation (RDBMS). TBA </p>

                <p><b>Properties:</b> For this case, we consider as a starting point three properties the transformation
                    should satisfy with respect to the correspondences between the two modeling languages.

                    <br/><br/>

                    <i>Property 1</i>: Non-persistent classes and non-top classes must not be transformed into a corresponding
                    table.

                    <br/><br/>

                    <i>Property 2</i>: All persistent top classes must be transformed into a corresponding table.

                    <br/><br/>

                    <i>Property 3</i>: Column duplicates are forbidden in the output models, i.e., there should not be two columns with the same name in one table.

                </p>

                <hr>

                <h2>UML activity diagrams to Petri nets Transformation Case (AD2PN)</h2>

                <p>
                    <b>Transformation:</b> This case concerns the mapping from UML activity diagrams into Petri nets as
                    the latter define the execution simulation of the former. For VOLT 2015, we will
                    consider the complete transformation presented in <a
                        href="http://dx.doi.org/10.1109/MoDRE.2012.6360083">Syriani and Ergin 2012</a>.
                </p>

                <p>
                    <b>Metamodels:</b> UML Activity Diagrams in graphical notation (AD) and Petri nets in graphical
                    notation (PN). TBA
                </p>

                <p>
                    <b>Properties:</b> For this case, we consider as a starting point three properties the
                    transformation should satisfy with respect to the analysis of the activity diagram.

                    <br/><br/>

                    <i>Property 1</i>: Exactly one transition is fireable from the initial PN model, as it encodes the
                    behavior of the initial node in AD.

                    <br/><br/>

                    <i>Property 2</i>: If an activity node has its current attribute set to true, then there must be a
                    token in the corresponding place.

                    <br/><br/>

                    <i>Property 3</i>: The entry, exit or transient transition corresponding to an activity node must be
                    L1-live: there exists a firing sequence in which each of these transitions can fire at least once.
                    Therefore, the resulting PN model is deadlock-free.

                </p>

                <hr>

                <h2>Pacman Simulation Transformation Case (PACSIM)</h2>

                <p>
                    <b>Transformation:</b> This case concerns the operational semantics of the Pacman DSML.
                    The original rule-based graph transformation description appeared in <a
                        href="http://dx.doi.org/10.1016/j.entcs.2005.12.018">Heckel 2006</a>.
                    For VOLT 2015, we refer to the slightly more complex implementation presented in <a
                        href="http://dx.doi.org/10.1007/s10270-011-0205-0">Syriani and Vangheluwe 2012</a>.
                </p>

                <p>
                    <b>Metamodel:</b> Pacman DSML from <a href="http://dx.doi.org/10.1007/s10270-011-0205-0"> Syriani
                    and Vangheluwe 2012</a>.
                </p>

                <p>
                    <b>Properties:</b> For this case, we consider as a starting point four properties the transformation
                    should satisfy with respect to the execution of an initial Pacman game configuration.

                    <br/><br/>

                    <i>Property 1</i>: All grid nodes containing a pellet (food) object must be reachable by the pacman
                    object.

                    <br/><br/>

                    <i>Property 2</i>: There exists a path where a ghost objects never kills pacman object.

                    <br/><br/>

                    <i>Property 3</i>: A pacman movement rule must be able successfully be applied before the K ghost
                    movement rules are applied. ALternatively, A pacman must move with a time interval I.

                    <br/><br/>

                    <i>Property 4</i>: The pacman object must move within a time interval I.
                </p>
        </tr>
        </tbody>
    </table>
</div>
</body>
</html>